r,s:rationals. (qeq(r; s))  (r = s) 

latex

Definitions	rationals, prop{i:l}, t  T, P  Q, P  Q, P  Q, P  Q, x:A. B(x), trans(T; x,y.E(x;y)), refl(T; x,y.E(x;y)), equiv_rel(T; x,y.E(x;y))
Lemmas	qeq wf, eqtt to assert, btrue wf, qeq-equiv, bool wf, rationals wf, qeq wf2, assert wf